We present the design of a new symmetric key management API for cryptographic devices intended to implement security protocols in distributed systems. Our API has a formal security policy expressed in terms of invariants under various threat scenarios, and proofs of security in the symbolic model. This sets it apart from previous APIs such as RSA PKCS#11, which are under-specified, lack a clear secuity policy and are often subject to attacks. Our design is based on the principle of explicitness: the security policy for a key must be given at creation time, and this policy is then included in any ciphertext containing the key. The policy is expressed in terms of a position in a hierarchy of keys and a set of agents. Our API also contains novel features such as the possibility of insisting on a freshness check before accepting an encrypted key for import. To show the applicability of our design, we give an algorithm for automatically instantiating the API commands for a given key management protocol. We demonstrate the algorithm on a set of symmetric key establishment protocols from the Clark-Jacob suite. We show that in the restricted mode of operation where freshness checks are required, some protocols from the test suite cannot be implemented: precisely those now known to be susceptible to replay attacks. This paper is an extended version of a paper published at the ESORICSconference in September 2009. It contains proofs of more fine-grainedsecurity properties than the original paper (for the same API), inparticular in the case where some but not all long-term keys on aparticular token are lost to the attacker. Since the original paper was submitted,another key management API with a security proof has appeared in theliterature due to Cachin and Chandran. This present paper contains a comparison ofthe two designs and their security properties, as well as a moredetailed comparison to other API designs.

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000D90 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 000D90 | SxmlIndent | more

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     Hal:hal-00881072
   |texte=   A Generic Security API for Symmetric Key Management on Cryptographic Devices
}}